(set-logic QF_UF)
(declare-sort u1 0)
(declare-sort u2 0)
(declare-fun Concat (Bool u1) u2)
(declare-fun y () Bool)
(declare-fun yn () u1)
(declare-fun yp () Bool)
(declare-fun yw () u2)
(assert (= yw (Concat yp yn)))
(assert (= yp (not y)))
(check-sat)
(exit)
